Modal interfaces: unifying interface automata and modal specifications,” in EMSOFT

This paper presents a unification of interface automata and modal specifications, two radically dissimilar models for in-terface theories. Interface automata is a game-based model, which allows to make assumptions on the environment and propose an optimistic view for composition: two compo-nents can be composed if there is an environment where they can work together. Modal specification is a language theo-retic account of a fragment of the modal mu-calculus logic that is more complete but which does not allow to distin-guish between the environment and the component. Partial unifications of these two frameworks have been explored re-cently. A first attempt by Larsen et al. considers modal in-terfaces, an extension of modal specifications that deals with compatibility issues in the composition operator. However, this composition operator is incorrect. A second attempt by Raclet et al. gives a different perspective, and emphasises on conjunction and residuation of modal specifications, in-cluding when interfaces have dissimilar alphabets, but disre-gards interface compatibility. The present paper contributes a thorougher unification of the two theories by correcting the modal interface composition operator presented in the paper by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing even further the comparison between interface automata, modal automata and modal in-terfaces